| Definitions |  x:A. B(x), Id, IdLnk, x:A  B(x), Dsys, x:A  B(x), P & Q, Feasible(D), False, P   Q,  A, {x:A| B(x)} ,  ,  b, Unit, left + right, M.(timed)state, Void, ma-prob(M;b), Outcome, b  dom(M.prob), if b then t else f fi , M.state,  , M sends on link l, queue(l;t), <a, b>, A  B,  , [], d-world(D;v;sched;dec;discrete), snds(l;t), source(l), M(i), M.dout2(l;tg),  x.A(x), Msg(M), type List, s = t, Type, t T, i  j , #$n, -n, n+m, n - m, a < b, upto(n), {i..j },  x:A.B(x), Top, Msg, m(l;t), [car / cdr], as @ bs, map(f;as), concat(ll),  ,  b, (i = j), P  Q, FinProbSpace, ||as||, i j < k, finite-type(T), Feasible(M), Atom$n, State(ds), case b of inl(x) => s(x) | inr(y) => t(y), S  T, suptype(S; T), onlnk(l;mss), m(i;t), t.2, timedState(ds), Knd, f(a), d-world-state(D;i), mlnk(m), a = b, filter(P;l),  x:A. B(x), P  Q, stutter-state(s), Msg(da), M.Msg, next-world-state(D;i;s;k;v), d-decl(D;i), M.V(k), read-state(s), M.dout(l,tg), M.din(l,tg), M.da(a), Valtype(da;k), M.sends(k,s,v), a = b, True,  T, P Q, msg(l;t;v), w.M, Action(i), rcvs(l;t), nth_tl(n;as) |
| Lemmas | nth tl wf, length wf1, nth tl nil, w-rcvs wf, w-action wf, msg wf, ma-dout wf, assert-eq-lnk, assert-eq-id, squash wf, true wf, filter filter reduce, eq id wf, ma-send-val wf, d-decl-subtype, ma-send-val-nil2, read-state wf, ma-msg wf, mlnk wf d, subtype rel self, d-comp-step, filter wf, eq lnk wf, mlnk wf, append nil sq, concat-cons, concat append, map wf, append wf, concat wf, w-ml wf, w-Msg wf, d-world wf, length wf nat, eqtt to assert, eqff to assert, iff transitivity, assert of bnot, not functionality wrt iff, assert of eq int, eq int wf, bnot wf, map append sq, int seg wf, upto wf, le wf, ge wf, not wf, assert wf, ma-sends-on wf, d-feasible wf, bool wf, ma-st wf, ifthenelse wf, ma-prob-dom wf, p-outcome wf, ma-prob wf, ma-tst wf, Id wf, nat wf, IdLnk wf, unit wf, dsys wf, nat properties, Msg wf, ma-dout2 wf, d-m wf, lsrc wf |
dec:(i,a:Id